Left Termination of the query pattern
ack(g,g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 189 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 181 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 PiDPToQDPProof (⇒, 5 ms)
        ↳9 QDP
        ↳10 QDPSizeChangeProof (⇔, 0 ms)
        ↳11 YES
    ↳12 PiDP
        ↳13 PiDPToQDPProof (⇒, 0 ms)
        ↳14 QDP
        ↳15 QDPSizeChangeProof (⇔, 0 ms)
        ↳16 YES

(0) Obligation:

Clauses:

ack(0, N, s(N)).
ack(s(M), 0, A) :- ack(M, s(0), A).
ack(s(M), s(N), A) :- ','(ack(s(M), N, A1), ack(M, A1, A)).

Query: ack(g,g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

ackB(X1, X2) :- ackC(X1, X2).
ackC(s(X1), X2) :- ackB(X1, X3).
ackC(s(X1), X2) :- ','(ackcB(X1, X3), ackD(X1, X3, X2)).
ackD(s(X1), 0, X2) :- ackC(X1, X2).
ackD(s(X1), s(X2), X3) :- ackD(s(X1), X2, X4).
ackD(s(X1), s(X2), X3) :- ','(ackcD(s(X1), X2, X4), ackD(X1, X4, X3)).
ackA(s(s(X1)), 0, X2) :- ackB(X1, X3).
ackA(s(s(X1)), 0, X2) :- ','(ackcB(X1, X3), ackA(X1, X3, X2)).
ackA(s(X1), s(0), X2) :- ackC(X1, X3).
ackA(s(X1), s(0), X2) :- ','(ackcC(X1, X3), ackA(X1, X3, X2)).
ackA(s(X1), s(s(X2)), X3) :- ackD(s(X1), X2, X4).
ackA(s(X1), s(s(X2)), X3) :- ','(ackcD(s(X1), X2, X4), ackD(X1, X4, X5)).
ackA(s(X1), s(s(X2)), X3) :- ','(ackcD(s(X1), X2, X4), ','(ackcD(X1, X4, X5), ackA(X1, X5, X3))).

Clauses:

ackcA(0, X1, s(X1)).
ackcA(s(0), 0, s(s(0))).
ackcA(s(s(X1)), 0, X2) :- ','(ackcB(X1, X3), ackcA(X1, X3, X2)).
ackcA(s(X1), s(0), X2) :- ','(ackcC(X1, X3), ackcA(X1, X3, X2)).
ackcA(s(X1), s(s(X2)), X3) :- ','(ackcD(s(X1), X2, X4), ','(ackcD(X1, X4, X5), ackcA(X1, X5, X3))).
ackcB(X1, X2) :- ackcC(X1, X2).
ackcC(0, s(s(0))).
ackcC(s(X1), X2) :- ','(ackcB(X1, X3), ackcD(X1, X3, X2)).
ackcD(0, X1, s(X1)).
ackcD(s(X1), 0, X2) :- ackcC(X1, X2).
ackcD(s(X1), s(X2), X3) :- ','(ackcD(s(X1), X2, X4), ackcD(X1, X4, X3)).

Afs:

ackA(x1, x2, x3)  =  ackA(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
ackA_in: (b,b,f)
ackB_in: (b,f)
ackC_in: (b,f)
ackcB_in: (b,f)
ackcC_in: (b,f)
ackcD_in: (b,b,f)
ackD_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

ACKA_IN_GGA(s(s(X1)), 0, X2) → U9_GGA(X1, X2, ackB_in_ga(X1, X3))
ACKA_IN_GGA(s(s(X1)), 0, X2) → ACKB_IN_GA(X1, X3)
ACKB_IN_GA(X1, X2) → U1_GA(X1, X2, ackC_in_ga(X1, X2))
ACKB_IN_GA(X1, X2) → ACKC_IN_GA(X1, X2)
ACKC_IN_GA(s(X1), X2) → U2_GA(X1, X2, ackB_in_ga(X1, X3))
ACKC_IN_GA(s(X1), X2) → ACKB_IN_GA(X1, X3)
ACKC_IN_GA(s(X1), X2) → U3_GA(X1, X2, ackcB_in_ga(X1, X3))
U3_GA(X1, X2, ackcB_out_ga(X1, X3)) → U4_GA(X1, X2, ackD_in_gga(X1, X3, X2))
U3_GA(X1, X2, ackcB_out_ga(X1, X3)) → ACKD_IN_GGA(X1, X3, X2)
ACKD_IN_GGA(s(X1), 0, X2) → U5_GGA(X1, X2, ackC_in_ga(X1, X2))
ACKD_IN_GGA(s(X1), 0, X2) → ACKC_IN_GA(X1, X2)
ACKD_IN_GGA(s(X1), s(X2), X3) → U6_GGA(X1, X2, X3, ackD_in_gga(s(X1), X2, X4))
ACKD_IN_GGA(s(X1), s(X2), X3) → ACKD_IN_GGA(s(X1), X2, X4)
ACKD_IN_GGA(s(X1), s(X2), X3) → U7_GGA(X1, X2, X3, ackcD_in_gga(s(X1), X2, X4))
U7_GGA(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → U8_GGA(X1, X2, X3, ackD_in_gga(X1, X4, X3))
U7_GGA(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → ACKD_IN_GGA(X1, X4, X3)
ACKA_IN_GGA(s(s(X1)), 0, X2) → U10_GGA(X1, X2, ackcB_in_ga(X1, X3))
U10_GGA(X1, X2, ackcB_out_ga(X1, X3)) → U11_GGA(X1, X2, ackA_in_gga(X1, X3, X2))
U10_GGA(X1, X2, ackcB_out_ga(X1, X3)) → ACKA_IN_GGA(X1, X3, X2)
ACKA_IN_GGA(s(X1), s(0), X2) → U12_GGA(X1, X2, ackC_in_ga(X1, X3))
ACKA_IN_GGA(s(X1), s(0), X2) → ACKC_IN_GA(X1, X3)
ACKA_IN_GGA(s(X1), s(0), X2) → U13_GGA(X1, X2, ackcC_in_ga(X1, X3))
U13_GGA(X1, X2, ackcC_out_ga(X1, X3)) → U14_GGA(X1, X2, ackA_in_gga(X1, X3, X2))
U13_GGA(X1, X2, ackcC_out_ga(X1, X3)) → ACKA_IN_GGA(X1, X3, X2)
ACKA_IN_GGA(s(X1), s(s(X2)), X3) → U15_GGA(X1, X2, X3, ackD_in_gga(s(X1), X2, X4))
ACKA_IN_GGA(s(X1), s(s(X2)), X3) → ACKD_IN_GGA(s(X1), X2, X4)
ACKA_IN_GGA(s(X1), s(s(X2)), X3) → U16_GGA(X1, X2, X3, ackcD_in_gga(s(X1), X2, X4))
U16_GGA(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → U17_GGA(X1, X2, X3, ackD_in_gga(X1, X4, X5))
U16_GGA(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → ACKD_IN_GGA(X1, X4, X5)
U16_GGA(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, X3, ackcD_in_gga(X1, X4, X5))
U18_GGA(X1, X2, X3, ackcD_out_gga(X1, X4, X5)) → U19_GGA(X1, X2, X3, ackA_in_gga(X1, X5, X3))
U18_GGA(X1, X2, X3, ackcD_out_gga(X1, X4, X5)) → ACKA_IN_GGA(X1, X5, X3)

The TRS R consists of the following rules:

ackcB_in_ga(X1, X2) → U28_ga(X1, X2, ackcC_in_ga(X1, X2))
ackcC_in_ga(0, s(s(0))) → ackcC_out_ga(0, s(s(0)))
ackcC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackcB_in_ga(X1, X3))
U29_ga(X1, X2, ackcB_out_ga(X1, X3)) → U30_ga(X1, X2, ackcD_in_gga(X1, X3, X2))
ackcD_in_gga(0, X1, s(X1)) → ackcD_out_gga(0, X1, s(X1))
ackcD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackcC_in_ga(X1, X2))
U31_gga(X1, X2, ackcC_out_ga(X1, X2)) → ackcD_out_gga(s(X1), 0, X2)
ackcD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackcD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackcD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackcD_out_gga(X1, X4, X3)) → ackcD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackcD_out_gga(X1, X3, X2)) → ackcC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackcC_out_ga(X1, X2)) → ackcB_out_ga(X1, X2)

The argument filtering Pi contains the following mapping:
ackA_in_gga(x1, x2, x3)  =  ackA_in_gga(x1, x2)
s(x1)  =  s(x1)
0  =  0
ackB_in_ga(x1, x2)  =  ackB_in_ga(x1)
ackC_in_ga(x1, x2)  =  ackC_in_ga(x1)
ackcB_in_ga(x1, x2)  =  ackcB_in_ga(x1)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
ackcC_in_ga(x1, x2)  =  ackcC_in_ga(x1)
ackcC_out_ga(x1, x2)  =  ackcC_out_ga(x1, x2)
U29_ga(x1, x2, x3)  =  U29_ga(x1, x3)
ackcB_out_ga(x1, x2)  =  ackcB_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
ackcD_in_gga(x1, x2, x3)  =  ackcD_in_gga(x1, x2)
ackcD_out_gga(x1, x2, x3)  =  ackcD_out_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x3)
U32_gga(x1, x2, x3, x4)  =  U32_gga(x1, x2, x4)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x4)
ackD_in_gga(x1, x2, x3)  =  ackD_in_gga(x1, x2)
ACKA_IN_GGA(x1, x2, x3)  =  ACKA_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
ACKB_IN_GA(x1, x2)  =  ACKB_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
ACKC_IN_GA(x1, x2)  =  ACKC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
ACKD_IN_GGA(x1, x2, x3)  =  ACKD_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKA_IN_GGA(s(s(X1)), 0, X2) → U9_GGA(X1, X2, ackB_in_ga(X1, X3))
ACKA_IN_GGA(s(s(X1)), 0, X2) → ACKB_IN_GA(X1, X3)
ACKB_IN_GA(X1, X2) → U1_GA(X1, X2, ackC_in_ga(X1, X2))
ACKB_IN_GA(X1, X2) → ACKC_IN_GA(X1, X2)
ACKC_IN_GA(s(X1), X2) → U2_GA(X1, X2, ackB_in_ga(X1, X3))
ACKC_IN_GA(s(X1), X2) → ACKB_IN_GA(X1, X3)
ACKC_IN_GA(s(X1), X2) → U3_GA(X1, X2, ackcB_in_ga(X1, X3))
U3_GA(X1, X2, ackcB_out_ga(X1, X3)) → U4_GA(X1, X2, ackD_in_gga(X1, X3, X2))
U3_GA(X1, X2, ackcB_out_ga(X1, X3)) → ACKD_IN_GGA(X1, X3, X2)
ACKD_IN_GGA(s(X1), 0, X2) → U5_GGA(X1, X2, ackC_in_ga(X1, X2))
ACKD_IN_GGA(s(X1), 0, X2) → ACKC_IN_GA(X1, X2)
ACKD_IN_GGA(s(X1), s(X2), X3) → U6_GGA(X1, X2, X3, ackD_in_gga(s(X1), X2, X4))
ACKD_IN_GGA(s(X1), s(X2), X3) → ACKD_IN_GGA(s(X1), X2, X4)
ACKD_IN_GGA(s(X1), s(X2), X3) → U7_GGA(X1, X2, X3, ackcD_in_gga(s(X1), X2, X4))
U7_GGA(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → U8_GGA(X1, X2, X3, ackD_in_gga(X1, X4, X3))
U7_GGA(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → ACKD_IN_GGA(X1, X4, X3)
ACKA_IN_GGA(s(s(X1)), 0, X2) → U10_GGA(X1, X2, ackcB_in_ga(X1, X3))
U10_GGA(X1, X2, ackcB_out_ga(X1, X3)) → U11_GGA(X1, X2, ackA_in_gga(X1, X3, X2))
U10_GGA(X1, X2, ackcB_out_ga(X1, X3)) → ACKA_IN_GGA(X1, X3, X2)
ACKA_IN_GGA(s(X1), s(0), X2) → U12_GGA(X1, X2, ackC_in_ga(X1, X3))
ACKA_IN_GGA(s(X1), s(0), X2) → ACKC_IN_GA(X1, X3)
ACKA_IN_GGA(s(X1), s(0), X2) → U13_GGA(X1, X2, ackcC_in_ga(X1, X3))
U13_GGA(X1, X2, ackcC_out_ga(X1, X3)) → U14_GGA(X1, X2, ackA_in_gga(X1, X3, X2))
U13_GGA(X1, X2, ackcC_out_ga(X1, X3)) → ACKA_IN_GGA(X1, X3, X2)
ACKA_IN_GGA(s(X1), s(s(X2)), X3) → U15_GGA(X1, X2, X3, ackD_in_gga(s(X1), X2, X4))
ACKA_IN_GGA(s(X1), s(s(X2)), X3) → ACKD_IN_GGA(s(X1), X2, X4)
ACKA_IN_GGA(s(X1), s(s(X2)), X3) → U16_GGA(X1, X2, X3, ackcD_in_gga(s(X1), X2, X4))
U16_GGA(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → U17_GGA(X1, X2, X3, ackD_in_gga(X1, X4, X5))
U16_GGA(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → ACKD_IN_GGA(X1, X4, X5)
U16_GGA(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, X3, ackcD_in_gga(X1, X4, X5))
U18_GGA(X1, X2, X3, ackcD_out_gga(X1, X4, X5)) → U19_GGA(X1, X2, X3, ackA_in_gga(X1, X5, X3))
U18_GGA(X1, X2, X3, ackcD_out_gga(X1, X4, X5)) → ACKA_IN_GGA(X1, X5, X3)

The TRS R consists of the following rules:

ackcB_in_ga(X1, X2) → U28_ga(X1, X2, ackcC_in_ga(X1, X2))
ackcC_in_ga(0, s(s(0))) → ackcC_out_ga(0, s(s(0)))
ackcC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackcB_in_ga(X1, X3))
U29_ga(X1, X2, ackcB_out_ga(X1, X3)) → U30_ga(X1, X2, ackcD_in_gga(X1, X3, X2))
ackcD_in_gga(0, X1, s(X1)) → ackcD_out_gga(0, X1, s(X1))
ackcD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackcC_in_ga(X1, X2))
U31_gga(X1, X2, ackcC_out_ga(X1, X2)) → ackcD_out_gga(s(X1), 0, X2)
ackcD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackcD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackcD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackcD_out_gga(X1, X4, X3)) → ackcD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackcD_out_gga(X1, X3, X2)) → ackcC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackcC_out_ga(X1, X2)) → ackcB_out_ga(X1, X2)

The argument filtering Pi contains the following mapping:
ackA_in_gga(x1, x2, x3)  =  ackA_in_gga(x1, x2)
s(x1)  =  s(x1)
0  =  0
ackB_in_ga(x1, x2)  =  ackB_in_ga(x1)
ackC_in_ga(x1, x2)  =  ackC_in_ga(x1)
ackcB_in_ga(x1, x2)  =  ackcB_in_ga(x1)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
ackcC_in_ga(x1, x2)  =  ackcC_in_ga(x1)
ackcC_out_ga(x1, x2)  =  ackcC_out_ga(x1, x2)
U29_ga(x1, x2, x3)  =  U29_ga(x1, x3)
ackcB_out_ga(x1, x2)  =  ackcB_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
ackcD_in_gga(x1, x2, x3)  =  ackcD_in_gga(x1, x2)
ackcD_out_gga(x1, x2, x3)  =  ackcD_out_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x3)
U32_gga(x1, x2, x3, x4)  =  U32_gga(x1, x2, x4)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x4)
ackD_in_gga(x1, x2, x3)  =  ackD_in_gga(x1, x2)
ACKA_IN_GGA(x1, x2, x3)  =  ACKA_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
ACKB_IN_GA(x1, x2)  =  ACKB_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
ACKC_IN_GA(x1, x2)  =  ACKC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
ACKD_IN_GGA(x1, x2, x3)  =  ACKD_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 17 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKB_IN_GA(X1, X2) → ACKC_IN_GA(X1, X2)
ACKC_IN_GA(s(X1), X2) → ACKB_IN_GA(X1, X3)
ACKC_IN_GA(s(X1), X2) → U3_GA(X1, X2, ackcB_in_ga(X1, X3))
U3_GA(X1, X2, ackcB_out_ga(X1, X3)) → ACKD_IN_GGA(X1, X3, X2)
ACKD_IN_GGA(s(X1), 0, X2) → ACKC_IN_GA(X1, X2)
ACKD_IN_GGA(s(X1), s(X2), X3) → ACKD_IN_GGA(s(X1), X2, X4)
ACKD_IN_GGA(s(X1), s(X2), X3) → U7_GGA(X1, X2, X3, ackcD_in_gga(s(X1), X2, X4))
U7_GGA(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → ACKD_IN_GGA(X1, X4, X3)

The TRS R consists of the following rules:

ackcB_in_ga(X1, X2) → U28_ga(X1, X2, ackcC_in_ga(X1, X2))
ackcC_in_ga(0, s(s(0))) → ackcC_out_ga(0, s(s(0)))
ackcC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackcB_in_ga(X1, X3))
U29_ga(X1, X2, ackcB_out_ga(X1, X3)) → U30_ga(X1, X2, ackcD_in_gga(X1, X3, X2))
ackcD_in_gga(0, X1, s(X1)) → ackcD_out_gga(0, X1, s(X1))
ackcD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackcC_in_ga(X1, X2))
U31_gga(X1, X2, ackcC_out_ga(X1, X2)) → ackcD_out_gga(s(X1), 0, X2)
ackcD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackcD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackcD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackcD_out_gga(X1, X4, X3)) → ackcD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackcD_out_gga(X1, X3, X2)) → ackcC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackcC_out_ga(X1, X2)) → ackcB_out_ga(X1, X2)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
ackcB_in_ga(x1, x2)  =  ackcB_in_ga(x1)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
ackcC_in_ga(x1, x2)  =  ackcC_in_ga(x1)
ackcC_out_ga(x1, x2)  =  ackcC_out_ga(x1, x2)
U29_ga(x1, x2, x3)  =  U29_ga(x1, x3)
ackcB_out_ga(x1, x2)  =  ackcB_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
ackcD_in_gga(x1, x2, x3)  =  ackcD_in_gga(x1, x2)
ackcD_out_gga(x1, x2, x3)  =  ackcD_out_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x3)
U32_gga(x1, x2, x3, x4)  =  U32_gga(x1, x2, x4)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x4)
ACKB_IN_GA(x1, x2)  =  ACKB_IN_GA(x1)
ACKC_IN_GA(x1, x2)  =  ACKC_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
ACKD_IN_GGA(x1, x2, x3)  =  ACKD_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(8) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKB_IN_GA(X1) → ACKC_IN_GA(X1)
ACKC_IN_GA(s(X1)) → ACKB_IN_GA(X1)
ACKC_IN_GA(s(X1)) → U3_GA(X1, ackcB_in_ga(X1))
U3_GA(X1, ackcB_out_ga(X1, X3)) → ACKD_IN_GGA(X1, X3)
ACKD_IN_GGA(s(X1), 0) → ACKC_IN_GA(X1)
ACKD_IN_GGA(s(X1), s(X2)) → ACKD_IN_GGA(s(X1), X2)
ACKD_IN_GGA(s(X1), s(X2)) → U7_GGA(X1, X2, ackcD_in_gga(s(X1), X2))
U7_GGA(X1, X2, ackcD_out_gga(s(X1), X2, X4)) → ACKD_IN_GGA(X1, X4)

The TRS R consists of the following rules:

ackcB_in_ga(X1) → U28_ga(X1, ackcC_in_ga(X1))
ackcC_in_ga(0) → ackcC_out_ga(0, s(s(0)))
ackcC_in_ga(s(X1)) → U29_ga(X1, ackcB_in_ga(X1))
U29_ga(X1, ackcB_out_ga(X1, X3)) → U30_ga(X1, ackcD_in_gga(X1, X3))
ackcD_in_gga(0, X1) → ackcD_out_gga(0, X1, s(X1))
ackcD_in_gga(s(X1), 0) → U31_gga(X1, ackcC_in_ga(X1))
U31_gga(X1, ackcC_out_ga(X1, X2)) → ackcD_out_gga(s(X1), 0, X2)
ackcD_in_gga(s(X1), s(X2)) → U32_gga(X1, X2, ackcD_in_gga(s(X1), X2))
U32_gga(X1, X2, ackcD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, ackcD_in_gga(X1, X4))
U33_gga(X1, X2, ackcD_out_gga(X1, X4, X3)) → ackcD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, ackcD_out_gga(X1, X3, X2)) → ackcC_out_ga(s(X1), X2)
U28_ga(X1, ackcC_out_ga(X1, X2)) → ackcB_out_ga(X1, X2)

The set Q consists of the following terms:

ackcB_in_ga(x0)
ackcC_in_ga(x0)
U29_ga(x0, x1)
ackcD_in_gga(x0, x1)
U31_gga(x0, x1)
U32_gga(x0, x1, x2)
U33_gga(x0, x1, x2)
U30_ga(x0, x1)
U28_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ACKC_IN_GA(s(X1)) → ACKB_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • ACKC_IN_GA(s(X1)) → U3_GA(X1, ackcB_in_ga(X1))
    The graph contains the following edges 1 > 1

  • ACKB_IN_GA(X1) → ACKC_IN_GA(X1)
    The graph contains the following edges 1 >= 1

  • ACKD_IN_GGA(s(X1), 0) → ACKC_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • U3_GA(X1, ackcB_out_ga(X1, X3)) → ACKD_IN_GGA(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • U7_GGA(X1, X2, ackcD_out_gga(s(X1), X2, X4)) → ACKD_IN_GGA(X1, X4)
    The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2

  • ACKD_IN_GGA(s(X1), s(X2)) → ACKD_IN_GGA(s(X1), X2)
    The graph contains the following edges 1 >= 1, 2 > 2

  • ACKD_IN_GGA(s(X1), s(X2)) → U7_GGA(X1, X2, ackcD_in_gga(s(X1), X2))
    The graph contains the following edges 1 > 1, 2 > 2

(11) YES

(12) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKA_IN_GGA(s(s(X1)), 0, X2) → U10_GGA(X1, X2, ackcB_in_ga(X1, X3))
U10_GGA(X1, X2, ackcB_out_ga(X1, X3)) → ACKA_IN_GGA(X1, X3, X2)
ACKA_IN_GGA(s(X1), s(0), X2) → U13_GGA(X1, X2, ackcC_in_ga(X1, X3))
U13_GGA(X1, X2, ackcC_out_ga(X1, X3)) → ACKA_IN_GGA(X1, X3, X2)
ACKA_IN_GGA(s(X1), s(s(X2)), X3) → U16_GGA(X1, X2, X3, ackcD_in_gga(s(X1), X2, X4))
U16_GGA(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, X3, ackcD_in_gga(X1, X4, X5))
U18_GGA(X1, X2, X3, ackcD_out_gga(X1, X4, X5)) → ACKA_IN_GGA(X1, X5, X3)

The TRS R consists of the following rules:

ackcB_in_ga(X1, X2) → U28_ga(X1, X2, ackcC_in_ga(X1, X2))
ackcC_in_ga(0, s(s(0))) → ackcC_out_ga(0, s(s(0)))
ackcC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackcB_in_ga(X1, X3))
U29_ga(X1, X2, ackcB_out_ga(X1, X3)) → U30_ga(X1, X2, ackcD_in_gga(X1, X3, X2))
ackcD_in_gga(0, X1, s(X1)) → ackcD_out_gga(0, X1, s(X1))
ackcD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackcC_in_ga(X1, X2))
U31_gga(X1, X2, ackcC_out_ga(X1, X2)) → ackcD_out_gga(s(X1), 0, X2)
ackcD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackcD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackcD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackcD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackcD_out_gga(X1, X4, X3)) → ackcD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackcD_out_gga(X1, X3, X2)) → ackcC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackcC_out_ga(X1, X2)) → ackcB_out_ga(X1, X2)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
ackcB_in_ga(x1, x2)  =  ackcB_in_ga(x1)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
ackcC_in_ga(x1, x2)  =  ackcC_in_ga(x1)
ackcC_out_ga(x1, x2)  =  ackcC_out_ga(x1, x2)
U29_ga(x1, x2, x3)  =  U29_ga(x1, x3)
ackcB_out_ga(x1, x2)  =  ackcB_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
ackcD_in_gga(x1, x2, x3)  =  ackcD_in_gga(x1, x2)
ackcD_out_gga(x1, x2, x3)  =  ackcD_out_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x3)
U32_gga(x1, x2, x3, x4)  =  U32_gga(x1, x2, x4)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x4)
ACKA_IN_GGA(x1, x2, x3)  =  ACKA_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(13) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKA_IN_GGA(s(s(X1)), 0) → U10_GGA(X1, ackcB_in_ga(X1))
U10_GGA(X1, ackcB_out_ga(X1, X3)) → ACKA_IN_GGA(X1, X3)
ACKA_IN_GGA(s(X1), s(0)) → U13_GGA(X1, ackcC_in_ga(X1))
U13_GGA(X1, ackcC_out_ga(X1, X3)) → ACKA_IN_GGA(X1, X3)
ACKA_IN_GGA(s(X1), s(s(X2))) → U16_GGA(X1, X2, ackcD_in_gga(s(X1), X2))
U16_GGA(X1, X2, ackcD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, ackcD_in_gga(X1, X4))
U18_GGA(X1, X2, ackcD_out_gga(X1, X4, X5)) → ACKA_IN_GGA(X1, X5)

The TRS R consists of the following rules:

ackcB_in_ga(X1) → U28_ga(X1, ackcC_in_ga(X1))
ackcC_in_ga(0) → ackcC_out_ga(0, s(s(0)))
ackcC_in_ga(s(X1)) → U29_ga(X1, ackcB_in_ga(X1))
U29_ga(X1, ackcB_out_ga(X1, X3)) → U30_ga(X1, ackcD_in_gga(X1, X3))
ackcD_in_gga(0, X1) → ackcD_out_gga(0, X1, s(X1))
ackcD_in_gga(s(X1), 0) → U31_gga(X1, ackcC_in_ga(X1))
U31_gga(X1, ackcC_out_ga(X1, X2)) → ackcD_out_gga(s(X1), 0, X2)
ackcD_in_gga(s(X1), s(X2)) → U32_gga(X1, X2, ackcD_in_gga(s(X1), X2))
U32_gga(X1, X2, ackcD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, ackcD_in_gga(X1, X4))
U33_gga(X1, X2, ackcD_out_gga(X1, X4, X3)) → ackcD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, ackcD_out_gga(X1, X3, X2)) → ackcC_out_ga(s(X1), X2)
U28_ga(X1, ackcC_out_ga(X1, X2)) → ackcB_out_ga(X1, X2)

The set Q consists of the following terms:

ackcB_in_ga(x0)
ackcC_in_ga(x0)
U29_ga(x0, x1)
ackcD_in_gga(x0, x1)
U31_gga(x0, x1)
U32_gga(x0, x1, x2)
U33_gga(x0, x1, x2)
U30_ga(x0, x1)
U28_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(15) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U10_GGA(X1, ackcB_out_ga(X1, X3)) → ACKA_IN_GGA(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • ACKA_IN_GGA(s(s(X1)), 0) → U10_GGA(X1, ackcB_in_ga(X1))
    The graph contains the following edges 1 > 1

  • U16_GGA(X1, X2, ackcD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, ackcD_in_gga(X1, X4))
    The graph contains the following edges 1 >= 1, 3 > 1, 2 >= 2, 3 > 2

  • U13_GGA(X1, ackcC_out_ga(X1, X3)) → ACKA_IN_GGA(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • U18_GGA(X1, X2, ackcD_out_gga(X1, X4, X5)) → ACKA_IN_GGA(X1, X5)
    The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2

  • ACKA_IN_GGA(s(X1), s(0)) → U13_GGA(X1, ackcC_in_ga(X1))
    The graph contains the following edges 1 > 1

  • ACKA_IN_GGA(s(X1), s(s(X2))) → U16_GGA(X1, X2, ackcD_in_gga(s(X1), X2))
    The graph contains the following edges 1 > 1, 2 > 2

(16) YES